(d )= d1d2 may be used to show that step trace
equivalence is not preserved under safe refinements as considered here. For step
bisimulation equivalence we conjecture that we do have preservation under safe
refinements.
We have investigated here how two well-established interleaving equivalences behave with respect to a restricted notion of action refinement. We have considered a class of refinements where events deciding choices are considered atomic. It turned out that interleaving trace semantics — neglecting the branching structure — is then still not preserved under refinements whereas interleaving bisimulation yields the desired preservation result.
It remains to be investigated what happens for other interleaving equivalences in
the linear time – branching time spectrum, e.g. for failure semantics. Another
interesting question is what happens for step semantics (where several actions
happening simultaneously are considered). The example a(bc| d ) versus
ab(c| d )+ a(b| d )c with
(d )= d1d2 may be used to show that step trace
equivalence is not preserved under safe refinements as considered here. For step
bisimulation equivalence we conjecture that we do have preservation under safe
refinements.
Acknowledgements
The idea to investigate refinements with atomic choice was
suggested by Manfred Broy. Three anonymous referees helped with their comments to improve the paper.